structure Proof1 =
struct
  structure A = Assert
  structure Asm = Assem
  
  type lemma = string
  type lab = string

  datatype prf_blk
    = WF_addr of Asm.reg * Asm.reg *((Asm.instr list) * prf_blk) * (lab * lab * lemma)
    | WF_subz of int * Asm.reg * ((Asm.instr list) * prf_blk) * (lab * lab * lemma)
    | WF_push of Asm.reg * ((Asm.instr list) * prf_blk) * (lab * lab * lemma)
    | WF_movr of Asm.reg * Asm.reg * ((Asm.instr list) * prf_blk) * (lab * lab * lemma)
    | WF_movld of int * Asm.reg * Asm.reg * ((Asm.instr list) * prf_blk) * (lab * lab * lemma)
    | WF_jmp of lab * (lab * lab * lemma)
    | WF_trivial

  datatype ptype
    = Int    (* Z *)
    | Label  (* label *)
    | Addr   (* Address *)
    | Hp     (* heap *)
    | Rf     (* register file *)
    | Sta    (* state *)
    | Reg    (* register *)
    | CB     (* code block *)
    | CT     (* code heap type *)
    | CH     (* code heap *)
    | Assert (* assertion *)
    | Prop of pterm  (* Proposition *)


  and pterm
    = Abs of (string * ptype) * pterm  (* abstraction, that is (arg_id, arg_type, function_body) *)
    | App of pterm * pterm  (* Application *)  
    | Var of string  (* variable *)

    | IntNum of int
    | Lab of int
    | AddrN of int 

    | ChTy of ((string * int) list)
    | Iseq of (Asm.instr list)
    | Ch of (Asm.instr list) list
    | Asst of string
    | St of pterm * pterm  (* (rf, hp) *)

    | True
    | Eax
    | Ebx
    | Ecx
    | Edx
    | Esi
    | Edi
    | Esp
    | Ebp

    | Plus of pterm * pterm (* e1 + e2 *)
    | Minus of pterm * pterm (* e1 - e2 *)
    | Times of pterm * pterm (* e1 * e2 *)

    | Gt of pterm * pterm  (* e1 > e2 *)
    | Ge of pterm * pterm  (* e1 >= e2 *)
    | Lt of pterm * pterm  (* e1 < e2 *)
    | Le of pterm * pterm  (* e1 <= e2 *)
    | Eq of pterm * pterm  (* e1 == e2 *)
    | Ne of pterm * pterm  (* e1 <> e2 *)

    | And of pterm * pterm  (* p1 /\ p2 *)
    | Or of pterm * pterm   (* p1 \/ p2 *)
    | Not of pterm (* ~p *)
end 
